Comments on “tautology testing with a generalized matrix reduction method”

AbstractBibel [1] has given a proof system for the propositional calculus called (generalized) matrix reduction. When matrix splitting is restricted to one literal at a time the system is the same as Galil's system [2] of enumeration dags. In fact the relation is even closer. The matrices produced by the reduction on a set of literals {I} are exactly the set of clauses appearing on a dag after |I| consecutive branches with substitute for the same literals. The clauses M1 (which do not appear in the matrices Mc) are exactly the clauses whose branches close with the empty clause Λ. Thus the saving in space is at most by a factor of |I|, but |I| is bounded from above by log2 M to ‘guarantee polynomial behaviour’. Hence Galil's system polynomially simulates matrix reduction and thus matrix reduction is also an exponential proof procedure